Nuprl Definition : connex
12,41
postcript
pdf
basic
Connex(
T
;
x
,
y
.
R
(
x
;
y
)) ==
x
,
y
:
T
.
R
(
x
;
y
)
R
(
y
;
x
)
latex
clarification:
basic
Connex(
T
;
x
,
y
.
R
(
x
;
y
)) ==
x
:
T
,
y
:
T
.
R
(
x
;
y
)
R
(
y
;
x
)
latex
Definitions
x
:
A
.
B
(
x
)
,
P
Q
FDL editor aliases
connex
origin
x, y:T. R(x;y) 
R(y;x)
x:T, y:T. R(x;y) R(y;x) x, y:T. R(x;y) R(y;x)
x:T, y:T. R(x;y) R(y;x) x:A. B(x) Q